package systemfnomabss

/**
   * Following typechecking as in Types and Programming Languages by Benjamin Pierce, chap 9-10-11
   *
   */

trait systemfTypeCheck extends TypeChecker {self: TypeChecker with TypeSubstitutionProvider with PrettyPrinter with AbstractSyntax=>
  case class VarBinding(ltype: LType) extends Binding 
  class TyVarNameBinding extends VarBinding(TyVar(Name("Error: encountered dummy type variable name of class TyVarBinding")))

  def typeOf(t:LTerm)  = Typer.fresh.typeOf(t)

  object Typer {
    def fresh() = new SystemFTyperFun {val ctx = new NameBindingContext[VarBinding,Name](Nil)}
  }

  trait Typer extends Function1[LTerm, LType] {
    type Ctx = NameBindingContext[VarBinding,Name]
    //type Ctx = StringBindingContext[VarBinding]
    val ctx: Ctx

    def rememberingTypeOfVar(n:Name, ty: LType) = {
      val ctxextended = ctx + (n, VarBinding(ty))
      create(ctxextended)
    }
    def rememberingTyVar(n:Name) = {
      val ctxextended = ctx + (n, new TyVarNameBinding)
      create(ctxextended)
    }
    def recallTypeOfVar(n:Name) = ctx(n) match {
      case Some(VarBinding(ty)) => {
        //var properdepthview = ty
        //List.range(0,offset+1).foreach {n => properdepthview = addingBinder(properdepthview)} //do i+1 timesty
      	//properdepthview
        ty
      }
      
      case None                 => throw new TypeExc("no varbinding found for variable with name "+n)
    }
    
    //def lookupVar(n: Int) = ctx(n)
    //def removingBinder(ty:LType) = ty

    def apply(t:LTerm):LType = { typeOf(t) }

    def typeOf(t: LTerm): LType
    def create(ctx: Ctx): Typer
  }

  
  
  
  trait SystemFTyperFun extends Typer {
    def create(initctx: Ctx)= {
      new SystemFTyperFun {val ctx = initctx}
    }
    def typeOf(t: LTerm)= t match {
         
      case Lit(n)     => TyInt()
      case Tru()      => TyBool()
      case Fls()      => TyBool()
      case Unit()     => TyUnit()
        
        case If(cond,pos,neg) => {
           if (TyBool() != typeOf(cond)) throw new TypeExc("conditional not boolean")
           val typpos = typeOf(pos)
           if ( typpos != typeOf(neg)) throw new TypeExc("branches of if differ in type: "+prettyPrint(typeOf(pos))+" vs "+prettyPrint(typeOf(neg)))
           typpos
        }

        case Let(conc, name \\body) => {
          val typeInsert = typeOf(conc)
          println("let binding: type "+typeInsert)
          rememberingTypeOfVar(name, typeInsert)(body)
        }
        
        case Var(n)       =>   { //T-Var
          recallTypeOfVar(n)
        }
        
        
        case Lam(ty,hint\\body) => {  //T-Abs
           TyArr(ty, rememberingTypeOfVar(hint,ty) (body) )
        }
        case App(tfun,targ)  => {  //T-App
          val funty = typeOf(tfun)
          val argty = typeOf(targ)
          funty match {
            case TyArr(fundom, funrange) => {
              //concrete and formal parameter types need to match
              if  (argty == fundom ) funrange 
              else throw new TypeExc("wrong application argument type: receive "+ (if(argty==null) "untyped" else prettyPrint(argty)) 
                +" but expect "+ (if(fundom==null)"" else prettyPrint(fundom) )+ " \n at "+prettyPrint(t))
             }
             case _ => throw new TypeExc("applying to non function type: arg ="+prettyPrint(targ)+" non-func ="+prettyPrint(tfun))
          }
        }
        
        
        case TLam(hint\\body)   => {  //T-TAbs
          //TyUniv(x, withExtendedScope(x, new TypeVarBinding(x)) typeOf(t))
          TyUniv(hint\\rememberingTyVar(hint) (body))
          //TyUniv(hint,this(body))
        }
        case TApp(t, ty) => {  //T-TApp
          val ttype = typeOf(t)
          ttype match {
            case TyUniv(x\\ty12) =>
              val result = substitutetype(ty).as(x).intotype(ty12)
              result
            case _  => throw new TypeExc("applying type to non universal type")
        }}
        
        case Pack(privtype,privimpl,sig) => { //T-Pack
          sig match {
          case TyExist(varname\\ty) =>
            val tyconcrete = substitutetype(privtype).as(varname).intotype(ty)
            val impltype = typeOf(privimpl)
            if (impltype == tyconcrete) TyExist(varname\\ty)
            else throw new TypeExc("type of "+privimpl+"="+impltype+" does not match public type "+ty)
          case _ => throw new TypeExc("cannot pack as non-existential type")
        }}
      case Unpack(pack,tyX\\Lam(tyXsynonym,varx\\body)) if TyVar(tyX) == (tyXsynonym)=> { //T-Unpack
        val impltype = typeOf(pack) //really look at it to force checks made under case Pack
        impltype match {
          case TyExist(tyX2\\tyvarx) =>//if tyX == tyX2 =>
           val tybody = rememberingTyVar(tyX).rememberingTypeOfVar(varx,tyvarx)(body)
           try {
           val tyextern  = tybody //view outside of double binder existential
           // we should not be referencing the newly bound var => only be referencing vars in the context outside of the binders
           println("unpackcheck: result.supp = "+tyextern.supp)
           if (tyextern.supp.contains(tyX2)) throw new TypeExc("leaking type variable out of import in "+t.toString)
           else tyextern
           } catch {case e: IllegalArgumentException =>throw new TypeExc("leaking type variable out of import in "+t.toString)
             throw new TypeExc("leaking type variable out of import in "+t.toString)
           }
       // case TyExist(a,b)                         => //not necessary, type variables may differ
       //    throw new TypeExc("cannot unpack existential type with different signature ")
          case _ => throw new TypeExc("cannot unpack non existential type ")
         
      }}
        
        
       
       case r@Record(fields)       => { 
          TyRecord(r.fieldsmap(typeOf))
       }
       case RecProj(t,label) => {
       typeOf(t) match {
         case r@TyRecord(fields) =>
              r.field(label)
         case _         => throw new TypeExc("trying to project field "+label+" of non-record:"+prettyPrint(t))
       }
       
       }
       
       case _ => throw new TypeExc("match error during typing: tree = "+t)
        
   }
  
  }
    
    
}

